As computer programs have become increasingly complex, the challenges of developing reliable software have become apparent. Modern software applications can contain millions of lines of code written by hundreds of developers, each with different sets of programming skills and styles. Debugging such applications is therefore a daunting task.
The basic concepts of software engineering are familiar to those skilled in the art. FIG. 1 shows a technique 100 for creating a computer program according to the prior art. First, at 110, a program is created/edited by one or more developers. Then, at 120, the program is debugged (e.g., using a debugging tool). At 130, if the program contains bugs to be fixed, the editing/debugging cycle continues. When the source code for a program is determined to be sufficiently bug-free, the source code is compiled into executable target code. FIG. 2 shows a block diagram of a system for compiling source code according to the prior art. A compiler 200 compiles source code written in a high-level language in source files 205 into target code 210 for execution on a computer. The target code 210 can be hardware-specific or generic to multiple hardware platforms. The compiler 200 can use, for example, lexical analysis, syntax analysis, code generation and code optimization to translate the source code into executable code. In addition, many compilers have debugging capabilities for detecting and describing errors at compile time.
The size and complexity of most commercially valuable software applications have made detecting every programming error (or “bug”) in such applications nearly impossible. To help manage software development and debugging tasks and to facilitate extensibility of large applications, software engineers have developed various techniques of analyzing, describing and/or documenting the behavior of programs to increase the number of bugs that can be found before a software product is sold or used.
For example, in one technique, source code is instrumented with additional code useful for checking expressions in C programs to determine whether each instance of a particular kind of program operation (string manipulations) is safe. The instrumentation is analyzed at compile time to assess the “cleanness” of each string manipulation. See Dor et al., “Cleanness Checking of String Manipulations in C Programs via Integer Analysis,” Proc. 8th Int'l Static Analysis Symposium (June 2001).
In other techniques, program specifications are written in specification languages that use different keywords and syntactic structures to describe the behavior of programs. Some specifications can be interpreted by compilers or debugging tools, helping to detect bugs that might not otherwise have been detected by other debugging tools or compilers. See, e.g., Evans et al., “LCLint: A Tool for Using Specifications to Check Code,” SIGSOFT Symposium on Foundations of Software Engineering (December 1994).
Some specification languages define “contracts” for programs that must be fulfilled in order for the program to work properly. See, e.g., Leavens and Baker, “Enhancing the Pre- and Post-condition Technique for More Expressive Specifications,” Proc. World Congress on Formal Methods in the Development of Computer Systems (September 1999). In general, a contract refers to a set of conditions. The set of conditions may include one or more preconditions and one or more postconditions. Contracts can be expressed as mappings from precondition states to postcondition states; if a given precondition holds, then the following postcondition must hold.
Preconditions are properties of the program that hold in the “pre” state of the callee (i.e., at the point in the execution when control is transferred to the callee). They typically describe expectations placed by the callee on the caller. Callers must guarantee that preconditions are satisfied, whereas callees may rely on preconditions, but not make any additional assumptions. Postconditions are properties of the program that hold in the “post” state of the callee (i.e., at the point in the execution when control is transferred back to the caller). They typically describe guarantees made to the caller by the callee. Callees must guarantee that postconditions are satisfied, whereas callers may rely on postconditions but may not make any additional assumptions.
Although many different specification languages have been previously developed, they tend to have shortcomings that fall into two categories. In some cases, specification languages are so complex that writing the specification is similar in terms of programmer burden to re-writing the program in a new language. This can be a heavy burden on programmers, whose primary task is to create programs rather than to describe how programs work. In other cases, specification languages are less complex but not expressive enough to describe the program in a useful way or to allow detection of a desirable range of errors.
Whatever the benefits of previous techniques, they do not have the advantages of the following tools and techniques.